LeanのFin 16のパターンマッチ
Lean
だと
Fin 15
と
Fin 16
からパターンマッチの挙動が変わる
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Pattern.20matching.20on.20Fin.20isn't.20exhaustive.20for.20large.20matches